<?php

class int {}
